H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 1.733 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ LR

mainModule List

((group :: [()] -> [[()]]) :: [()] -> [[()]])

module List where

import qualified Maybe
import qualified Prelude

group :: Eq a => [a] -> [[a]]

group

groupBy (==)

groupBy :: (a -> a -> Bool) -> [a] -> [[a]]

groupBy

_ []

[]

groupBy

eq (x : xs)

(x : ys) : groupBy eq zs

where

vv10

span (eq x) xs

(\(ys,_) ->ys) vv10

(\(_,zs) ->zs) vv10

module Maybe where

import qualified List
import qualified Prelude

Lambda Reductions:
The following Lambda expression

\(_,zs)→zs

is transformed to

zs0 (_,zs) = zs

The following Lambda expression

\(ys,_)→ys

is transformed to

ys0 (ys,_) = ys

The following Lambda expression

\(_,zs)→zs

is transformed to

zs1 (_,zs) = zs

The following Lambda expression

\(ys,_)→ys

is transformed to

ys1 (ys,_) = ys

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

mainModule List

((group :: [()] -> [[()]]) :: [()] -> [[()]])

module List where

import qualified Maybe
import qualified Prelude

group :: Eq a => [a] -> [[a]]

group

groupBy (==)

groupBy :: (a -> a -> Bool) -> [a] -> [[a]]

groupBy

_ []

[]

groupBy

eq (x : xs)

(x : ys) : groupBy eq zs

where

vv10

span (eq x) xs

ys0 vv10

ys0

(ys,_)

zs0 vv10

zs0

(_,zs)

module Maybe where

import qualified List
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern

xs@(wu : wv)

is replaced by the following term

wu : wv

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule List

((group :: [()] -> [[()]]) :: [()] -> [[()]])

module List where

import qualified Maybe
import qualified Prelude

group :: Eq a => [a] -> [[a]]

group

groupBy (==)

groupBy :: (a -> a -> Bool) -> [a] -> [[a]]

groupBy

vw []

[]

groupBy

eq (x : xs)

(x : ys) : groupBy eq zs

where

vv10

span (eq x) xs

ys0 vv10

ys0

(ys,vx)

zs0 vv10

zs0

(vy,zs)

module Maybe where

import qualified List
import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

The following Function with conditions

span p [] = ([],[])

span p (wu : wv)

| p wu

= (wu : ys,zs)

| otherwise

= ([],wu : wv)

where

vu43 = span p wv

ys = ys1 vu43

ys1 (ys,wx) = ys

zs = zs1 vu43

zs1 (ww,zs) = zs

is transformed to

span p [] = span3 p []

span p (wu : wv) = span2 p (wu : wv)

span2 p (wu : wv) =

span1 p wu wv (p wu)

where

span0 p wu wv True = ([],wu : wv)

span1 p wu wv True = (wu : ys,zs)

span1 p wu wv False = span0 p wu wv otherwise

vu43 = span p wv

ys = ys1 vu43

ys1 (ys,wx) = ys

zs = zs1 vu43

zs1 (ww,zs) = zs

span3 p [] = ([],[])

span3 xv xw = span2 xv xw

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

mainModule List

((group :: [()] -> [[()]]) :: [()] -> [[()]])

module List where

import qualified Maybe
import qualified Prelude

group :: Eq a => [a] -> [[a]]

group

groupBy (==)

groupBy :: (a -> a -> Bool) -> [a] -> [[a]]

groupBy

vw []

[]

groupBy

eq (x : xs)

(x : ys) : groupBy eq zs

where

vv10

span (eq x) xs

ys0 vv10

ys0

(ys,vx)

zs0 vv10

zs0

(vy,zs)

module Maybe where

import qualified List
import qualified Prelude

Let/Where Reductions:
The bindings of the following Let/Where expression

(x : ys) : groupBy eq zs

where

vv10 = span (eq x) xs

ys = ys0 vv10

ys0 (ys,vx) = ys

zs = zs0 vv10

zs0 (vy,zs) = zs

are unpacked to the following functions on top level

groupByZs xx xy xz = groupByZs0 xx xy xz (groupByVv10 xx xy xz)

groupByYs0 xx xy xz (ys,vx) = ys

groupByZs0 xx xy xz (vy,zs) = zs

groupByVv10 xx xy xz = span (xx xy) xz

groupByYs xx xy xz = groupByYs0 xx xy xz (groupByVv10 xx xy xz)

The bindings of the following Let/Where expression

span1 p wu wv (p wu)

where

span0 p wu wv True = ([],wu : wv)

span1 p wu wv True = (wu : ys,zs)

span1 p wu wv False = span0 p wu wv otherwise

vu43 = span p wv

ys = ys1 vu43

ys1 (ys,wx) = ys

zs = zs1 vu43

zs1 (ww,zs) = zs

are unpacked to the following functions on top level

span2Ys yu yv = span2Ys1 yu yv (span2Vu43 yu yv)

span2Zs yu yv = span2Zs1 yu yv (span2Vu43 yu yv)

span2Zs1 yu yv (ww,zs) = zs

span2Span1 yu yv p wu wv True = (wu : span2Ys yu yv,span2Zs yu yv)

span2Span1 yu yv p wu wv False = span2Span0 yu yv p wu wv otherwise

span2Vu43 yu yv = span yu yv

span2Span0 yu yv p wu wv True = ([],wu : wv)

span2Ys1 yu yv (ys,wx) = ys

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

mainModule List

(group :: [()] -> [[()]])

module List where

import qualified Maybe
import qualified Prelude

group :: Eq a => [a] -> [[a]]

group

groupBy (==)

groupBy :: (a -> a -> Bool) -> [a] -> [[a]]

groupBy	vw []	=	[]
groupBy	eq (x : xs)	=	(x : groupByYs eq x xs) : groupBy eq (groupByZs eq x xs)

groupByVv10

xx xy xz

span (xx xy) xz

groupByYs

xx xy xz

groupByYs0 xx xy xz (groupByVv10 xx xy xz)

groupByYs0

xx xy xz (ys,vx)

groupByZs

xx xy xz

groupByZs0 xx xy xz (groupByVv10 xx xy xz)

groupByZs0

xx xy xz (vy,zs)

module Maybe where

import qualified List
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="group",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="group yw3",fontsize=16,color="black",shape="triangle"];3 -> 4[label="",style="solid", color="black", weight=3];
4[label="groupBy (==) yw3",fontsize=16,color="burlywood",shape="triangle"];77[label="yw3/yw30 : yw31",fontsize=10,color="white",style="solid",shape="box"];4 -> 77[label="",style="solid", color="burlywood", weight=9];
77 -> 5[label="",style="solid", color="burlywood", weight=3];
78[label="yw3/[]",fontsize=10,color="white",style="solid",shape="box"];4 -> 78[label="",style="solid", color="burlywood", weight=9];
78 -> 6[label="",style="solid", color="burlywood", weight=3];
5[label="groupBy (==) (yw30 : yw31)",fontsize=16,color="black",shape="box"];5 -> 7[label="",style="solid", color="black", weight=3];
6[label="groupBy (==) []",fontsize=16,color="black",shape="box"];6 -> 8[label="",style="solid", color="black", weight=3];
7[label="(yw30 : groupByYs (==) yw30 yw31) : groupBy (==) (groupByZs (==) yw30 yw31)",fontsize=16,color="green",shape="box"];7 -> 9[label="",style="dashed", color="green", weight=3];
7 -> 10[label="",style="dashed", color="green", weight=3];
8[label="[]",fontsize=16,color="green",shape="box"];9[label="groupByYs (==) yw30 yw31",fontsize=16,color="black",shape="box"];9 -> 11[label="",style="solid", color="black", weight=3];
10 -> 4[label="",style="dashed", color="red", weight=0];
10[label="groupBy (==) (groupByZs (==) yw30 yw31)",fontsize=16,color="magenta"];10 -> 12[label="",style="dashed", color="magenta", weight=3];
11[label="groupByYs0 (==) yw30 yw31 (groupByVv10 (==) yw30 yw31)",fontsize=16,color="black",shape="box"];11 -> 13[label="",style="solid", color="black", weight=3];
12[label="groupByZs (==) yw30 yw31",fontsize=16,color="black",shape="box"];12 -> 14[label="",style="solid", color="black", weight=3];
13[label="groupByYs0 (==) yw30 yw31 (span ((==) yw30) yw31)",fontsize=16,color="burlywood",shape="box"];80[label="yw31/yw310 : yw311",fontsize=10,color="white",style="solid",shape="box"];13 -> 80[label="",style="solid", color="burlywood", weight=9];
80 -> 15[label="",style="solid", color="burlywood", weight=3];
81[label="yw31/[]",fontsize=10,color="white",style="solid",shape="box"];13 -> 81[label="",style="solid", color="burlywood", weight=9];
81 -> 16[label="",style="solid", color="burlywood", weight=3];
14[label="groupByZs0 (==) yw30 yw31 (groupByVv10 (==) yw30 yw31)",fontsize=16,color="black",shape="box"];14 -> 17[label="",style="solid", color="black", weight=3];
15[label="groupByYs0 (==) yw30 (yw310 : yw311) (span ((==) yw30) (yw310 : yw311))",fontsize=16,color="black",shape="box"];15 -> 18[label="",style="solid", color="black", weight=3];
16[label="groupByYs0 (==) yw30 [] (span ((==) yw30) [])",fontsize=16,color="black",shape="box"];16 -> 19[label="",style="solid", color="black", weight=3];
17[label="groupByZs0 (==) yw30 yw31 (span ((==) yw30) yw31)",fontsize=16,color="burlywood",shape="box"];82[label="yw31/yw310 : yw311",fontsize=10,color="white",style="solid",shape="box"];17 -> 82[label="",style="solid", color="burlywood", weight=9];
82 -> 20[label="",style="solid", color="burlywood", weight=3];
83[label="yw31/[]",fontsize=10,color="white",style="solid",shape="box"];17 -> 83[label="",style="solid", color="burlywood", weight=9];
83 -> 21[label="",style="solid", color="burlywood", weight=3];
18[label="groupByYs0 (==) yw30 (yw310 : yw311) (span2 ((==) yw30) (yw310 : yw311))",fontsize=16,color="black",shape="box"];18 -> 22[label="",style="solid", color="black", weight=3];
19[label="groupByYs0 (==) yw30 [] (span3 ((==) yw30) [])",fontsize=16,color="black",shape="box"];19 -> 23[label="",style="solid", color="black", weight=3];
20[label="groupByZs0 (==) yw30 (yw310 : yw311) (span ((==) yw30) (yw310 : yw311))",fontsize=16,color="black",shape="box"];20 -> 24[label="",style="solid", color="black", weight=3];
21[label="groupByZs0 (==) yw30 [] (span ((==) yw30) [])",fontsize=16,color="black",shape="box"];21 -> 25[label="",style="solid", color="black", weight=3];
22[label="groupByYs0 (==) yw30 (yw310 : yw311) (span2Span1 ((==) yw30) yw311 ((==) yw30) yw310 yw311 ((==) yw30 yw310))",fontsize=16,color="burlywood",shape="box"];84[label="yw30/()",fontsize=10,color="white",style="solid",shape="box"];22 -> 84[label="",style="solid", color="burlywood", weight=9];
84 -> 26[label="",style="solid", color="burlywood", weight=3];
23[label="groupByYs0 (==) yw30 [] ([],[])",fontsize=16,color="black",shape="box"];23 -> 27[label="",style="solid", color="black", weight=3];
24[label="groupByZs0 (==) yw30 (yw310 : yw311) (span2 ((==) yw30) (yw310 : yw311))",fontsize=16,color="black",shape="box"];24 -> 28[label="",style="solid", color="black", weight=3];
25[label="groupByZs0 (==) yw30 [] (span3 ((==) yw30) [])",fontsize=16,color="black",shape="box"];25 -> 29[label="",style="solid", color="black", weight=3];
26[label="groupByYs0 (==) () (yw310 : yw311) (span2Span1 ((==) ()) yw311 ((==) ()) yw310 yw311 ((==) () yw310))",fontsize=16,color="burlywood",shape="box"];85[label="yw310/()",fontsize=10,color="white",style="solid",shape="box"];26 -> 85[label="",style="solid", color="burlywood", weight=9];
85 -> 30[label="",style="solid", color="burlywood", weight=3];
27[label="[]",fontsize=16,color="green",shape="box"];28[label="groupByZs0 (==) yw30 (yw310 : yw311) (span2Span1 ((==) yw30) yw311 ((==) yw30) yw310 yw311 ((==) yw30 yw310))",fontsize=16,color="burlywood",shape="box"];86[label="yw30/()",fontsize=10,color="white",style="solid",shape="box"];28 -> 86[label="",style="solid", color="burlywood", weight=9];
86 -> 31[label="",style="solid", color="burlywood", weight=3];
29[label="groupByZs0 (==) yw30 [] ([],[])",fontsize=16,color="black",shape="box"];29 -> 32[label="",style="solid", color="black", weight=3];
30[label="groupByYs0 (==) () (() : yw311) (span2Span1 ((==) ()) yw311 ((==) ()) () yw311 ((==) () ()))",fontsize=16,color="black",shape="box"];30 -> 33[label="",style="solid", color="black", weight=3];
31[label="groupByZs0 (==) () (yw310 : yw311) (span2Span1 ((==) ()) yw311 ((==) ()) yw310 yw311 ((==) () yw310))",fontsize=16,color="burlywood",shape="box"];87[label="yw310/()",fontsize=10,color="white",style="solid",shape="box"];31 -> 87[label="",style="solid", color="burlywood", weight=9];
87 -> 34[label="",style="solid", color="burlywood", weight=3];
32[label="[]",fontsize=16,color="green",shape="box"];33[label="groupByYs0 (==) () (() : yw311) (span2Span1 ((==) ()) yw311 ((==) ()) () yw311 True)",fontsize=16,color="black",shape="box"];33 -> 35[label="",style="solid", color="black", weight=3];
34[label="groupByZs0 (==) () (() : yw311) (span2Span1 ((==) ()) yw311 ((==) ()) () yw311 ((==) () ()))",fontsize=16,color="black",shape="box"];34 -> 36[label="",style="solid", color="black", weight=3];
35[label="groupByYs0 (==) () (() : yw311) (() : span2Ys ((==) ()) yw311,span2Zs ((==) ()) yw311)",fontsize=16,color="black",shape="box"];35 -> 37[label="",style="solid", color="black", weight=3];
36[label="groupByZs0 (==) () (() : yw311) (span2Span1 ((==) ()) yw311 ((==) ()) () yw311 True)",fontsize=16,color="black",shape="box"];36 -> 38[label="",style="solid", color="black", weight=3];
37[label="() : span2Ys ((==) ()) yw311",fontsize=16,color="green",shape="box"];37 -> 39[label="",style="dashed", color="green", weight=3];
38[label="groupByZs0 (==) () (() : yw311) (() : span2Ys ((==) ()) yw311,span2Zs ((==) ()) yw311)",fontsize=16,color="black",shape="box"];38 -> 40[label="",style="solid", color="black", weight=3];
39[label="span2Ys ((==) ()) yw311",fontsize=16,color="black",shape="triangle"];39 -> 41[label="",style="solid", color="black", weight=3];
40[label="span2Zs ((==) ()) yw311",fontsize=16,color="black",shape="triangle"];40 -> 42[label="",style="solid", color="black", weight=3];
41[label="span2Ys1 ((==) ()) yw311 (span2Vu43 ((==) ()) yw311)",fontsize=16,color="black",shape="box"];41 -> 43[label="",style="solid", color="black", weight=3];
42[label="span2Zs1 ((==) ()) yw311 (span2Vu43 ((==) ()) yw311)",fontsize=16,color="black",shape="box"];42 -> 44[label="",style="solid", color="black", weight=3];
43[label="span2Ys1 ((==) ()) yw311 (span ((==) ()) yw311)",fontsize=16,color="burlywood",shape="box"];88[label="yw311/yw3110 : yw3111",fontsize=10,color="white",style="solid",shape="box"];43 -> 88[label="",style="solid", color="burlywood", weight=9];
88 -> 45[label="",style="solid", color="burlywood", weight=3];
89[label="yw311/[]",fontsize=10,color="white",style="solid",shape="box"];43 -> 89[label="",style="solid", color="burlywood", weight=9];
89 -> 46[label="",style="solid", color="burlywood", weight=3];
44[label="span2Zs1 ((==) ()) yw311 (span ((==) ()) yw311)",fontsize=16,color="burlywood",shape="box"];90[label="yw311/yw3110 : yw3111",fontsize=10,color="white",style="solid",shape="box"];44 -> 90[label="",style="solid", color="burlywood", weight=9];
90 -> 47[label="",style="solid", color="burlywood", weight=3];
91[label="yw311/[]",fontsize=10,color="white",style="solid",shape="box"];44 -> 91[label="",style="solid", color="burlywood", weight=9];
91 -> 48[label="",style="solid", color="burlywood", weight=3];
45[label="span2Ys1 ((==) ()) (yw3110 : yw3111) (span ((==) ()) (yw3110 : yw3111))",fontsize=16,color="black",shape="box"];45 -> 49[label="",style="solid", color="black", weight=3];
46[label="span2Ys1 ((==) ()) [] (span ((==) ()) [])",fontsize=16,color="black",shape="box"];46 -> 50[label="",style="solid", color="black", weight=3];
47[label="span2Zs1 ((==) ()) (yw3110 : yw3111) (span ((==) ()) (yw3110 : yw3111))",fontsize=16,color="black",shape="box"];47 -> 51[label="",style="solid", color="black", weight=3];
48[label="span2Zs1 ((==) ()) [] (span ((==) ()) [])",fontsize=16,color="black",shape="box"];48 -> 52[label="",style="solid", color="black", weight=3];
49[label="span2Ys1 ((==) ()) (yw3110 : yw3111) (span2 ((==) ()) (yw3110 : yw3111))",fontsize=16,color="black",shape="box"];49 -> 53[label="",style="solid", color="black", weight=3];
50[label="span2Ys1 ((==) ()) [] (span3 ((==) ()) [])",fontsize=16,color="black",shape="box"];50 -> 54[label="",style="solid", color="black", weight=3];
51[label="span2Zs1 ((==) ()) (yw3110 : yw3111) (span2 ((==) ()) (yw3110 : yw3111))",fontsize=16,color="black",shape="box"];51 -> 55[label="",style="solid", color="black", weight=3];
52[label="span2Zs1 ((==) ()) [] (span3 ((==) ()) [])",fontsize=16,color="black",shape="box"];52 -> 56[label="",style="solid", color="black", weight=3];
53[label="span2Ys1 ((==) ()) (yw3110 : yw3111) (span2Span1 ((==) ()) yw3111 ((==) ()) yw3110 yw3111 ((==) () yw3110))",fontsize=16,color="burlywood",shape="box"];92[label="yw3110/()",fontsize=10,color="white",style="solid",shape="box"];53 -> 92[label="",style="solid", color="burlywood", weight=9];
92 -> 57[label="",style="solid", color="burlywood", weight=3];
54[label="span2Ys1 ((==) ()) [] ([],[])",fontsize=16,color="black",shape="box"];54 -> 58[label="",style="solid", color="black", weight=3];
55[label="span2Zs1 ((==) ()) (yw3110 : yw3111) (span2Span1 ((==) ()) yw3111 ((==) ()) yw3110 yw3111 ((==) () yw3110))",fontsize=16,color="burlywood",shape="box"];93[label="yw3110/()",fontsize=10,color="white",style="solid",shape="box"];55 -> 93[label="",style="solid", color="burlywood", weight=9];
93 -> 59[label="",style="solid", color="burlywood", weight=3];
56[label="span2Zs1 ((==) ()) [] ([],[])",fontsize=16,color="black",shape="box"];56 -> 60[label="",style="solid", color="black", weight=3];
57[label="span2Ys1 ((==) ()) (() : yw3111) (span2Span1 ((==) ()) yw3111 ((==) ()) () yw3111 ((==) () ()))",fontsize=16,color="black",shape="box"];57 -> 61[label="",style="solid", color="black", weight=3];
58[label="[]",fontsize=16,color="green",shape="box"];59[label="span2Zs1 ((==) ()) (() : yw3111) (span2Span1 ((==) ()) yw3111 ((==) ()) () yw3111 ((==) () ()))",fontsize=16,color="black",shape="box"];59 -> 62[label="",style="solid", color="black", weight=3];
60[label="[]",fontsize=16,color="green",shape="box"];61[label="span2Ys1 ((==) ()) (() : yw3111) (span2Span1 ((==) ()) yw3111 ((==) ()) () yw3111 True)",fontsize=16,color="black",shape="box"];61 -> 63[label="",style="solid", color="black", weight=3];
62[label="span2Zs1 ((==) ()) (() : yw3111) (span2Span1 ((==) ()) yw3111 ((==) ()) () yw3111 True)",fontsize=16,color="black",shape="box"];62 -> 64[label="",style="solid", color="black", weight=3];
63 -> 65[label="",style="dashed", color="red", weight=0];
63[label="span2Ys1 ((==) ()) (() : yw3111) (() : span2Ys ((==) ()) yw3111,span2Zs ((==) ()) yw3111)",fontsize=16,color="magenta"];63 -> 66[label="",style="dashed", color="magenta", weight=3];
63 -> 67[label="",style="dashed", color="magenta", weight=3];
64 -> 68[label="",style="dashed", color="red", weight=0];
64[label="span2Zs1 ((==) ()) (() : yw3111) (() : span2Ys ((==) ()) yw3111,span2Zs ((==) ()) yw3111)",fontsize=16,color="magenta"];64 -> 69[label="",style="dashed", color="magenta", weight=3];
64 -> 70[label="",style="dashed", color="magenta", weight=3];
66 -> 40[label="",style="dashed", color="red", weight=0];
66[label="span2Zs ((==) ()) yw3111",fontsize=16,color="magenta"];66 -> 71[label="",style="dashed", color="magenta", weight=3];
67 -> 39[label="",style="dashed", color="red", weight=0];
67[label="span2Ys ((==) ()) yw3111",fontsize=16,color="magenta"];67 -> 72[label="",style="dashed", color="magenta", weight=3];
65[label="span2Ys1 ((==) ()) (() : yw3111) (() : yw5,yw4)",fontsize=16,color="black",shape="triangle"];65 -> 73[label="",style="solid", color="black", weight=3];
69 -> 40[label="",style="dashed", color="red", weight=0];
69[label="span2Zs ((==) ()) yw3111",fontsize=16,color="magenta"];69 -> 74[label="",style="dashed", color="magenta", weight=3];
70 -> 39[label="",style="dashed", color="red", weight=0];
70[label="span2Ys ((==) ()) yw3111",fontsize=16,color="magenta"];70 -> 75[label="",style="dashed", color="magenta", weight=3];
68[label="span2Zs1 ((==) ()) (() : yw3111) (() : yw7,yw6)",fontsize=16,color="black",shape="triangle"];68 -> 76[label="",style="solid", color="black", weight=3];
71[label="yw3111",fontsize=16,color="green",shape="box"];72[label="yw3111",fontsize=16,color="green",shape="box"];73[label="() : yw5",fontsize=16,color="green",shape="box"];74[label="yw3111",fontsize=16,color="green",shape="box"];75[label="yw3111",fontsize=16,color="green",shape="box"];76[label="yw6",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                        ↳ QDPSizeChangeProof

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_span2Ys(:(@0, yw3111)) → new_span2Zs(yw3111)
new_span2Zs(:(@0, yw3111)) → new_span2Ys(yw3111)
new_span2Zs(:(@0, yw3111)) → new_span2Zs(yw3111)
new_span2Ys(:(@0, yw3111)) → new_span2Ys(yw3111)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_span2Zs(:(@0, yw3111)) → new_span2Ys(yw3111)
The graph contains the following edges 1 > 1
new_span2Zs(:(@0, yw3111)) → new_span2Zs(yw3111)
The graph contains the following edges 1 > 1
new_span2Ys(:(@0, yw3111)) → new_span2Ys(yw3111)
The graph contains the following edges 1 > 1
new_span2Ys(:(@0, yw3111)) → new_span2Zs(yw3111)
The graph contains the following edges 1 > 1

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

new_groupBy(:(yw30, yw31)) → new_groupBy(new_groupByZs0(yw30, yw31))

The TRS R consists of the following rules:

new_span2Zs0(:(@0, yw3111)) → new_span2Zs1(yw3111, new_span2Ys0(yw3111), new_span2Zs0(yw3111))
new_span2Ys1(yw3111, yw5, yw4) → :(@0, yw5)
new_groupByZs0(yw30, []) → []
new_groupByZs0(@0, :(@0, yw311)) → new_span2Zs0(yw311)
new_span2Ys0([]) → []
new_span2Zs1(yw3111, yw7, yw6) → yw6
new_span2Zs0([]) → []
new_span2Ys0(:(@0, yw3111)) → new_span2Ys1(yw3111, new_span2Ys0(yw3111), new_span2Zs0(yw3111))

The set Q consists of the following terms:

new_span2Zs1(x0, x1, x2)
new_groupByZs0(@0, :(@0, x0))
new_span2Ys0([])
new_span2Zs0(:(@0, x0))
new_span2Ys1(x0, x1, x2)
new_span2Ys0(:(@0, x0))
new_span2Zs0([])
new_groupByZs0(x0, [])

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_groupBy(:(yw30, yw31)) → new_groupBy(new_groupByZs0(yw30, yw31))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25]:

POL(:(x₁, x₂)) = 1 + x₁
POL(@0) = 0
POL([]) = 0
POL(new_groupBy(x₁)) = x₁
POL(new_groupByZs0(x₁, x₂)) = 0
POL(new_span2Ys0(x₁)) = 1 + x₁
POL(new_span2Ys1(x₁, x₂, x₃)) = 1
POL(new_span2Zs0(x₁)) = 0
POL(new_span2Zs1(x₁, x₂, x₃)) = x₃

The following usable rules [17] were oriented:

new_span2Zs0([]) → []
new_span2Zs0(:(@0, yw3111)) → new_span2Zs1(yw3111, new_span2Ys0(yw3111), new_span2Zs0(yw3111))
new_groupByZs0(yw30, []) → []
new_span2Zs1(yw3111, yw7, yw6) → yw6
new_groupByZs0(@0, :(@0, yw311)) → new_span2Zs0(yw311)
new_span2Ys1(yw3111, yw5, yw4) → :(@0, yw5)
new_span2Ys0(:(@0, yw3111)) → new_span2Ys1(yw3111, new_span2Ys0(yw3111), new_span2Zs0(yw3111))

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

new_span2Zs0(:(@0, yw3111)) → new_span2Zs1(yw3111, new_span2Ys0(yw3111), new_span2Zs0(yw3111))
new_span2Ys1(yw3111, yw5, yw4) → :(@0, yw5)
new_groupByZs0(yw30, []) → []
new_groupByZs0(@0, :(@0, yw311)) → new_span2Zs0(yw311)
new_span2Ys0([]) → []
new_span2Zs1(yw3111, yw7, yw6) → yw6
new_span2Zs0([]) → []
new_span2Ys0(:(@0, yw3111)) → new_span2Ys1(yw3111, new_span2Ys0(yw3111), new_span2Zs0(yw3111))

The set Q consists of the following terms:

new_span2Zs1(x0, x1, x2)
new_groupByZs0(@0, :(@0, x0))
new_span2Ys0([])
new_span2Zs0(:(@0, x0))
new_span2Ys1(x0, x1, x2)
new_span2Ys0(:(@0, x0))
new_span2Zs0([])
new_groupByZs0(x0, [])

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

span2Span1	yu yv p wu wv True	= (wu : span2Ys yu yv,span2Zs yu yv)
span2Span1	yu yv p wu wv False	= span2Span0 yu yv p wu wv otherwise